1. $T$ : Type
\\[0ex]2. $L$ : $T$ List
\\[0ex]3. $x$ : $T$
\\[0ex]4. $y$ : $T$
\\[0ex]5. $i$ : \{0..($\parallel$$L$$\parallel$ {-} 1)$^{-}$\}
\\[0ex]6. $x$ = $L$[$i$]
\\[0ex]7. $y$ = $L$[($i$+1)]
\\[0ex]8. $\forall$${\it i@}_{0}$:\{0..1$^{-}$\}. if (${\it i@}_{0}$ =$_{0}$ 0) then $i$ else $i$+1 fi  $<$ if (${\it i@}_{0}$+1 =$_{0}$ 0) then $i$ else $i$+1 fi 
\\[0ex]9. $j$ : \{0..2$^{-}$\}
\\[0ex]$\vdash$  [$x$; $y$][$j$] = $L$[if ($j$ =$_{0}$ 0) then $i$ else $i$+1 fi ]